Step of Proof: outr_wf
12,41
postcript
pdf
Inference at
*
1
1
I
of proof for Lemma
outr
wf
:
1.
A
: Type
2.
B
: Type
3.
x1
:
A
4. False
outr(inl
x1
)
B
latex
by (Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term)
latex
.
Definitions
False
origin